Definitions | x:A B(x), t T, x:A. B(x), S T, Type, A, s = t, left + right, Top, f(a), P  Q, do-apply(f;x), b, , ff, can-apply(f;x), ,  b, x:A B(x), P & Q, P   Q, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, x f y, a < b, [d] , p   q, p  q, p  q, tt, , Unit, x.A(x), suptype(S; T), if b then t else f fi , Void, x:A.B(x), f o g , False, inr x , Decision, True, inl x |